Definitions	sq_type(T), Knd, x:A. B(x), P  Q, guard(T), t  T, prop{i:l}, x. t(x), tt, b, if b then t else f fi , True, t.1, x(s), t.2, ff, False
Lemmas	IdLnk sq, IdLnk wf, Id sq, Id wf, pi1 wf, pi2 wf, btrue wf, bfalse wf, assert wf